package sat;

import java.util.Vector;
import sat.convenience.Solution;
import sat.exceptions.ParseException;

public class FormulaCNF {
    private Vector<ClauseCNF> clauses;
    
    /**
     * Konwertuje formułę w postaci CNF z reprezentacji tekstowej na wewnętrzną
     * @param formula reprezentacja tekstowa
     * @throws ParseException 
     */
    public FormulaCNF(String formula) throws ParseException{
        clauses = new Vector<ClauseCNF>();
        parseString(formula);
    }
    
    /**
     * Zwraca zbiór literałów (bez powtórzeń) występujących w formule (zaniedbując
     * ew. negacje)
     * @return zbiór literałów wraz z przypisanymi im początkowo wartościami (wszystkie fałsz)
     */
    public Solution getUniqueLiterals(){
        Solution resultSet = new Solution();
        for(int i=0; i<clauses.size(); ++i){
            for(int j=0; j<clauses.get(i).getStringLiterals().size(); ++j){
                resultSet.put(clauses.get(i).getStringLiterals().get(j), Boolean.FALSE);
            }
        }
        return resultSet;
    }
    
    /**
     * Sprawdza, czy podane rozwiązanie spełnia formułę.
     * @param values
     * @return 
     */
    public boolean evaluate(Solution values){
        for(int i=0; i<clauses.size(); ++i){
            if(!clauses.get(i).evaluate(values)){
                return false;
            }
        }
        return true;
    }
    
    /**
     * Prywatna metoda realizująca parsowanie tekstu celem konwersji formuły
     * do reprezentacji wewnętrznej.
     * @param formula tekstowa postać formuły
     * @throws ParseException 
     */
    private void parseString(String formula) throws ParseException{
        String[] tokens = formula.split("&");
        for(int i=0; i<tokens.length; ++i){
            clauses.add(new ClauseCNF(tokens[i]));
        }
    }
    
    public String toString(){
        StringBuffer sb = new StringBuffer();
        for(int i=0; i<clauses.size(); ++i){
            if(i!=0){
                sb.append(" & ");
            }
            sb.append(clauses.get(i).toString());
        }
        return sb.toString();
    }
    
    /**
     * Zwraca odsetek klauzul spełnionych danym podstawieniem
     * @param solution podstawienie
     * @return odsetek wyrażony jako liczba 0-1
     */
    public float getTrueClausesPercentage(Solution solution){
        int t = 0;
        for(int i=0; i<clauses.size(); ++i){
            t+=(clauses.get(i).evaluate(solution)?1:0);
        }
        return t/(float)clauses.size();
    }
    
    /**
     * Zwraca odsetek spełnionych klauzul wyrażony jako stosunek łącznej długości
     * spełnionych klauzul do łącznej długości wszystkich klauzul ("odsetek ważony")
     * @param solution podstawienie
     * @return odsetek wyrażony jako liczba 0-1
     */
    public float getWeighedTrueClausesPercentage(Solution solution){
        int t=0, s=0;
        for(int i=0; i<clauses.size(); ++i){
            int literals = clauses.get(i).getLiteralsCount();
            s+=literals;
            t+=(clauses.get(i).evaluate(solution)?literals:0);
        }
        return t/(float)s;
    }
}
